de Bruijnインデックス
De Bruijn Index
「どぶらうん」と読む
引数の出現順番に合わせて、その順番を引数名にする感じ
見づらいが簡素に書けるのが嬉しい
例
λx.xはλ.0
λxy.yxはλ.λ.1 0
変換手順
示すまでもないがmrsekut.icon
元のラムダ式の変数名を自然数に順番に変える
λxy.yx→λ0.λ1.01
λにある数値を消す
λ0.λ1.01→λ.λ.01
自由変数を含む場合
出現する自由変数に予め記号と数値の対応を定義しておく
$ \Gamma=x\to2,y\to1,z\to0
出現する束縛変数の個数に↑を足して変数を表現する
例
λw.ywは束縛変数はwの一つなので$ \Gammaに1足して、yは2になるのでλ.2 0
λw.λa.xは束縛変数は2つなので、$ \Gammaに2足して、xは4になるのでλ.λ.4
代入操作
indexが1ずれる
ref TaPL.icon pp.59-60
関数適用
数値を更新する必要がある
ref TaPL.icon pp.60-61
参考